/*Z OK 内核页表、中断栈数据结构 */

/*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: GPL-2.0-only
 */

#include <arch/model/statedata.h>
/*Z 1G巨页只需要两级页表 */
/* The privileged kernel mapping PD & PT */
pml4e_t x64KSKernelPML4[BIT(PML4_INDEX_BITS)] ALIGN(BIT(seL4_PML4Bits)) VISIBLE;/*Z 内核一级页表。只需1页 */
pdpte_t x64KSKernelPDPT[BIT(PDPT_INDEX_BITS)] ALIGN(BIT(seL4_PDPTBits));        /*Z 内核二级页表。只需1页 */
#ifdef CONFIG_HUGE_PAGE
pde_t x64KSKernelPD[BIT(PD_INDEX_BITS)] ALIGN(BIT(seL4_PageDirBits));           /*Z 内核三级页表。1页，用于4K页映射设备或2M页 */
#else
pde_t x64KSKernelPDs[BIT(PDPT_INDEX_BITS)][BIT(PD_INDEX_BITS)] ALIGN(BIT(seL4_PageDirBits));/*Z 内核三级页表。512页 */
#endif
pte_t x64KSKernelPT[BIT(PT_INDEX_BITS)] ALIGN(BIT(seL4_PageTableBits));         /*Z 内核四级页表。1页，用于4K页映射设备 */

#ifdef CONFIG_KERNEL_SKIM_WINDOW
pml4e_t x64KSSKIMPML4[BIT(PML4_INDEX_BITS)] ALIGN(BIT(seL4_PML4Bits));  /*Z 内核滑动窗口空间，一级页表，1页 */
pdpte_t x64KSSKIMPDPT[BIT(PDPT_INDEX_BITS)] ALIGN(BIT(seL4_PDPTBits));  /*Z 内核滑动窗口空间，二级页表，1页 */
pde_t x64KSSKIMPD[BIT(PD_INDEX_BITS)] ALIGN(BIT(seL4_PageDirBits));     /*Z 内核滑动窗口空间，三级页表，1页 */
#endif

#ifdef CONFIG_KERNEL_SKIM_WINDOW
UP_STATE_DEFINE(word_t, x64KSCurrentUserCR3);
#else
UP_STATE_DEFINE(cr3_t, x64KSCurrentCR3);
#endif
/*Z 各core中断栈。大小只有8X8字节（实际用的是6X8，另2个是为了凑齐cacheline */
word_t x64KSIRQStack[CONFIG_MAX_NUM_NODES][IRQ_STACK_SIZE + 2] ALIGN(64) VISIBLE SKIM_BSS;
